\section{Conclusions}

This paper presents \tname{}, an approach to assist model checker
users in finding data race errors.  The general goal of our approach
is to increase responsiveness of model checkers; enabling users to
take action before a potentially long search for actual errors
finishes.  \tname{} predicts likely races from the events monitored
during the exploration of distinct thread interleavings.  We analyzed
\numSubjects{} subjects of various sources and sizes previously used
in the analysis of concurrent systems.  Results indicate that the
overhead in runtime compared to a regular state-space exploration is
low on average, the number of false positives is low, and the reports
are given most often very fast to the user.\Comment{ \tname{} provides
  a new dimension to existing predictive analysis: the analysis of
  multiple traces.}  The approach of \tname{} is lightweight as to
handle high volume of information and the demand to not severely
affect overall exploration time (to find actual errors).  To the best
of our knowledge, this is the first paper that exploits the synergy
between predictive analysis and program model checking.  Our
implementation and the subjects we used in our experiments are
available from the following link:

\vspace{1ex}
\begin{center}
\url{http://pan.cin.ufpe.br/rabbit}
\end{center}

\Comment{
\vspace{1ex}\noindent\textbf{Acknowledgments.}~We thank Elton Alves,
Filipe Ximenes, Weslley Torres, Gustavo Henrique and Mateus Borges for
the support with the experiments and Saswat Anand and Milos Gligoric
for comments on earlier versions of the paper.\Comment{Fernanda
  d'Amorim for the comments on earlier versions of this paper} This
work was partially supported by the National Institute of Science and
Technology for Software Engineering ({\small INES}:
{\url{http://www.ines.org.br}} ) and FACEPE grant \#
IBPG-0779-1.03/09.
}

% LocalWords:  interleavings runtime Alves Filipe Weslley Henrique Mateus Anand
% LocalWords:  Saswat Milos Gligoric d'Amorim FACEPE
